include "arithmetics/nat.ma".
include "basics/deqsets.ma". 
include "basics/lists/listb.ma".

(********************************************)
(********** ATOMI *************)
inductive Atom: Type[0] ≝
   Name  : nat → Atom
 | CoName: nat → Atom .

(* Atom: notation and interpretation *)
interpretation "Name" 'Name n = (Name n).
notation "hvbox(𝔸 \sub n)" with precedence 90 for @{ 'Name $n }.

(* Negative atom: notation and interpretation *)
notation "hvbox(𝔹 \sub n)" with precedence 90 for @{ 'CoName $n }.
interpretation "CoName" 'CoName n = (CoName n).

(* Per definire insiemi di nomi e co-nomi tramite funzione caratteristica
come nel seguente esempio:
definition exSetB ≝ { 𝔸 \sub 2 } ∪ {𝔹 \sub 2} .
occorre avere 'include "basics/sets.ma"' .
Non seguirò questa strada perché mi pare servano strutture in cui cercare 
effettivamente gli atomi. Ovvero servono liste su insiemi con equivalenza
decidibile, come indicato da chapter5.ma e chapter6.ma. *)

definition Atomeqb ≝ λa,b:Atom.
  match a with 
  [ Name   n ⇒ match b with 
               [ Name   m ⇒ (eqb n m)
               | _        ⇒ false]
  | CoName n ⇒ match b with 
               [ CoName m ⇒ (eqb n m)
               | _        ⇒ false]].
               
notation < "a == b" non associative 
      with precedence 45 for @{Atomeqb $a $b }.

lemma Atomeqb_true: ∀a,b. iff (Atomeqb a b = true) (a = b).
(* Ho guardato la dimostrazione del lemma 
   beqitem_true in chapter7.ma del tutorial ed ho
   provato a non saltare neanche un passo. *)
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .

(* Grazie al lemma precedente ho che gli Atomi formano un insieme
con equivalenza decidibile. *)
definition AtomDeqSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

(* A me viene da dire che si dovrebbe poter dimostrare:
   lemma  Atomeqb_false: ∀a,b:AtomDeqSet. (eqb_false AtomDeqSet a b).
ma lo statement non piace a Matita. 
La sua 'forma esplosa' è qui sotto dimostrata semplicemente copiando 
la dimostrazione di:
   lemma eqb_false: ∀S:DeqSet.∀a,b:S. (eqb ? a b) = false ↔ a ≠ b.
in basics/deqsets.ma la quale è dimostrabile toglendo #S. *)
lemma Atomeqb_false: ∀a,b:AtomDeqSet. (eqb AtomDeqSet a b) = false ↔ a ≠ b.
#a #b % #H 
  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  ] qed.

(* Segue la decidibilità, anche questa copiata da basics/deqsets.ma 
ed adattata. *)
lemma Atomdec_eq: ∀a,b:AtomDeqSet. a = b ∨ a ≠ b.
#a #b cases (true_or_false (eqb ? a b)) #H
  [%1 @(\P H) | %2 @(\Pf H)] qed.

(* Prima di procedere nello sfruttare AtomDeqSet, definisco la negazione
su Atom, in modo da collegare ogni nome col suo co-nome. Immagino che poi
servirà... .*)
definition Atomneg ≝ λa:Atom.
  match a with 
  [ Name   n ⇒ CoName n
  | CoName n ⇒ Name   n  ].

lemma Atomneg_idem : ∀ a: Atom. Atomneg (Atomneg a) = a.
#a cases a #N normalize @refl qed .

(* Tra le definizioni e gli statements del chapter5.ma posso scegliere
di istanziare con AtomDeqSet quelle utili al fine di usare il tipo
list AtomDeqSet come insieme di elementi in AtomDeqSet. *)
let rec Atom_memb (x:AtomDeqSet) (l: list AtomDeqSet) on l  ≝
  match l with
  [ nil ⇒ false
  | cons a tl ⇒ (x == a) ∨ (Atom_memb x tl)
  ].

(* notation < "∈ x l" non associative 
      with precedence 90 for @{'Atom_memb $x $l}.
interpretation "list Atom membership" 'Atom_memb a l = (Atom_memb ? a l). *)

(* If we want to represent finite sets as lists, we should
avoid duplicating elements. Atom_uniqueb checks this property.
Ho dimostrato alcune delle proprietà legate all'uso delle 
list AtmDeqSet come insiemi, ma in realtà è inutile perché
tali liste devono essere usate come multi-insieme. *)
let rec Atom_uniqueb (l: list AtomDeqSet) on l : bool ≝
  match l with 
  [ nil ⇒ true
  | cons a tl ⇒ notb (Atom_memb a tl) ∧ (Atom_uniqueb tl) ].

(* (Atom_unique_append l1 l2) adds l1 in front of l2, preserving unicity. *)
let rec Atom_unique_append (l1,l2: list AtomDeqSet) on l1 ≝
  match l1 with
  [ nil       ⇒ l2
  | cons a tl ⇒ let r ≝ Atom_unique_append tl l2 in
                 if Atom_memb a r then r else a::r   ].

lemma Atom_memb_unique_append: 
 ∀a:AtomDeqSet.∀ l1,l2:list AtomDeqSet. 
  Atom_memb a (Atom_unique_append l1 l2) = true 
     → (Atom_memb a l1= true) ∨ (Atom_memb a l2 = true).
(* La dimostrazione del
   lemma memb_unique_append: 
    ∀S,a,l1,l2.   memb S a (unique_append S l1 l2) = true → 
                     memb S a l1= true ∨ memb S a l2 = true.
   non è scritta nel modo più generale ed ho dovuto 
   riorganizzare oculatamente le normalizzazioni e i passi
   che consideravano i vari casi, pena l'impossibilità di 
   applicare l'ipotesi induttiva. *)
normalize (* Fondamentale per semplificare nello stesso modo
              i tipi di a, l1 ed l2. *)
#a #l1 elim l1 [#l2 #H normalize in H; %2 @H]
#b #tl cases a cases b (* Piazzare i casi per a e b 
                            in questo punto è fondamentale
                            per applicare l'induzione . *)
#n #m #Hind -a -b #l2 normalize 
[1:cases (Atom_memb  (𝔸 \sub n)  (Atom_unique_append tl l2))
   normalize 
   [1: #H cases (eqb m n) normalize 
       [ %1 @refl | lapply H @Hind]
   |2: cases (eqb m n) normalize
       [#H %1 @refl  | @Hind ]  
   ]
|2: (* Il cases nel caso seguente è molto istruttivo 
       a proposito dell'uiso di Matita: evidenzia come
       visitare i rami alternativi nella definizione di una
       funzione, grazie ai valori risultanti
       dalla valutazione dell'espressione argomento
       di cases.  *)
    cases (Atom_memb (𝔹 \sub n) (Atom_unique_append tl l2))
    normalize @Hind
|3: cases (Atom_memb (𝔸 \sub n) (Atom_unique_append tl l2))
    normalize @Hind
|4: cases (Atom_memb (𝔹 \sub n) (Atom_unique_append tl l2))
    normalize 
    [1: #H cases (eqb m n) normalize 
        [ %1 @refl | lapply H @Hind]
    |2: cases (eqb m n) normalize
        [#H %1 @refl  | @Hind ]  ]
] qed. 

lemma Atom_unique_append_elim: ∀P: AtomDeqSet → Prop.∀l1,l2. 
  (∀x. Atom_memb x l1 = true → P x) → (∀x. Atom_memb x l2 = true → P x) →
    ∀x. Atom_memb x (Atom_unique_append l1 l2) = true → P x. 
#P #l1 #l2 #Hl1 #Hl2 #x #membx cases (Atom_memb_unique_append … membx) /2/ 
qed.

lemma Atom_unique_append_unique: ∀l1,l2. Atom_uniqueb l2 = true →
  Atom_uniqueb (Atom_unique_append l1 l2) = true.
#l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
cases (true_or_false … (Atom_memb a (Atom_unique_append tl l2))) 
#H >H normalize [@Hind //] >H normalize @Hind //
qed.


(* È necessario poter confrontare l1,l2: list AtomDeqSeq, trattando
ciascuna come multi-insieme. Due liste l1 ed l2 rappresentano lo
stesso multi-insieme se hanno lunghezza identica, ovvero se |l1| = |l2| 
(la funzione length è già in basics/lists/list.ma) e 
∀e di l1. #occ(e) in l1 = #occ(e) in l2.
Ne dovrebbe conseguire

ListAtomDeqSeteqb l l'

da usarsi per definire Structureqb abbozzata più sotto. 

Il primo passo è saper ricavare l'insieme di elementi di AtomDeqSeq
in ogni list AtomDeqSeq. A questo serve (per fortuna!) unique_append 
in basics/lists/listb.ma.
Qui sotto ci sono due esempi di funzionamento di unique_append. La 
certificazione che unique_append trasoforma una lista in un insieme è:
 lemma unique_append_unique: 
  ∀S,l1,l2. uniqueb S l2 = true →
            uniqueb S (unique_append S l1 l2) = true.
dimosatrato in basics/lists/listb.ma. *)

lemma unique_append_e1:
unique_append AtomDeqSet ((𝔸 \sub 1)::(𝔸 \sub 1)::[]) [ ] = [𝔸 \sub 1] .
normalize // qed.
  
lemma unique_append_e2:
unique_append AtomDeqSet ((𝔸 \sub 1)::(𝔸 \sub 2)::(𝔸 \sub 1)::[]) [] = 
                         ((𝔸 \sub 2)::(𝔸 \sub 1)::[]) .
normalize // qed.

(* Dato che non si sa mai, dimostro un principio di induzione sulle liste con
elementi in un DeqSet, che non mi pare esistere. *)
lemma list_ind : ∀T:DeqSet.∀l:list T.∀P:list T → Prop.
  (P []) → (∀t,h. P t → P (h::t)) → P l.
#T #l #P #Pnil #Pcons elim l [@Pnil | -Pnil #H #T @Pcons ] qed.

let rec occ_number (A:DeqSet) (e:A) (l:list A) on l: nat ≝
match l with
[ nil ⇒ 0
| cons h t ⇒ if (memb A e [h]) then (S (occ_number A e t))
                                else (  occ_number A e t)  ].

lemma occ_number_ex1:
occ_number AtomDeqSet (𝔸 \sub 1) 
                      ((𝔸 \sub 1)::(𝔸 \sub 2)::(𝔸 \sub 1)::[])  = 2 .
normalize @refl qed.

lemma occ_number_ex2:
occ_number AtomDeqSet (𝔸 \sub 3) ((𝔸 \sub 1)::(𝔸 \sub 2)::[])  = 0 .
normalize @refl qed.

(* Cose ragionevoli che mi vengono in mente di provare su
occ_number. 
lemma occ_number_not_memb: 
∀A.∀e.∀l. ((memb ? e l) = false) → occ_number A e l = 0. 

lemma occ_number_empty: 
∀A.∀e.∀l. l = [ ] → occ_number A e l = 0.  *)

definition occ_number_eqb ≝ 
λA:DeqSet.λe:A.λl1,l2:list A.
eqb (occ_number A e l1) (occ_number A e l2).

let rec ListAtomeqb_core  
(s:list AtomDeqSet)   (* Insieme dei nomi e co-nomi 
                          di riferimento. *) 
 (l1,l2:list AtomDeqSet) on s ≝
  match s with
  [nil ⇒ true
  |cons h t ⇒ ((occ_number_eqb ? h l1 l2) ∧
               (occ_number_eqb ? h l1 l2)) ∧
              (ListAtomeqb_core t l1 l2) ].


lemma ListAtomeqb_core_true: 
∀s,a,b: list AtomDeqSet. iff (ListAtomeqb_core s a b = true) (a = b).
#s inversion s
[#snil normalize #a #b % destruct /2/ 
|
] qed .
 #a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .



definition ListAtomeqb ≝ λl1,l2:list AtomDeqSet.
  (eqb (|l1|) (|l2|)) ∧
  (ListAtomeqb_core (Atom_unique_append l1 []) l1 l2).
(* check ListAtomeqb. *)

lemma ListAtomeqb_ex1:
ListAtomeqb ((𝔸 \sub 1)::[]) 
            ((𝔸 \sub 1)::[]) = true.
normalize // qed .

lemma ListAtomeqb_ex2:
ListAtomeqb ((𝔸 \sub 1)::[]) 
            ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) = false.
normalize // qed .

lemma ListAtomeqb_ex3:
ListAtomeqb ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
            ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) = true.
normalize // qed .

lemma ListAtomeqb_ex4:
ListAtomeqb ((𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
            ((𝔸 \sub 2)::(𝔸 \sub 1)::[]) = true.
normalize // qed .

lemma ListAtomeqb_ex5:
ListAtomeqb ((𝔸 \sub 2)::(𝔸 \sub 1)::(𝔸 \sub 2)::[]) 
            ((𝔸 \sub 1)::(𝔸 \sub 2)::(𝔸 \sub 2)::[]) = true.
normalize // qed .

(* Manca almeno .. *)
lemma ListAtomeqb_true: 
 ∀a,b: list AtomDeqSet. iff (ListAtomeqb a b = true) (a = b).
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .
               
notation < "a ≐ b" non associative 
      with precedence 45 for @{ListAtomeqb $a $b }.



(*****************************)
(******** OPERATORI **********)
inductive  Operator : Type[0] ≝
|  par : Operator
|  seq : Operator
|  cop : Operator .

definition Operatoreqb ≝ λa,b:Operator.
  match a with 
  [ par ⇒ match b with [ par ⇒ true | _ ⇒ false]
  | seq ⇒ match b with [ seq ⇒ true | _ ⇒ false]
  | cop ⇒ match b with [ cop ⇒ true | _ ⇒ false]].

lemma Operatoreqb_true: ∀a,b. 
   iff (Operatoreqb a b = true) (a = b).
#a cases a -a #b cases b -b %
[1,3,5,7,9,11,13,15,17: #H normalize in H; destruct @refl
|2,4,6,8,10,12,14,16,18: #H normalize destruct @refl
] qed .

definition OperatorDeqSet ≝ mk_DeqSet Operator Operatoreqb Operatoreqb_true.

lemma Operatoreqb_false: 
   ∀a,b:OperatorDeqSet. (eqb ? a b) = false ↔ a ≠ b.
#a #b % #H 
  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq  @(\b H1)
  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  ] qed.

lemma Opeartordec_eq: ∀a,b:OperatorDeqSet. a = b ∨ a ≠ b.
#a #b cases (true_or_false (eqb ? a b)) #H
  [%1 @(\P H) | %2 @(\Pf H)] qed.

(*****************************)
(******** Strutture **********)
inductive Structure : Type[0] ≝
|  unit   : Structure
|  sbase  : Operator → list AtomDeqSet → Structure
|  sind   : Operator → list Structure  → Structure .

definition Structureqb ≝ λa,b:Structure.
  match a with 
  [ unit      ⇒ match b with 
                 [ unit ⇒ true | _    ⇒ false]
  | sbase o l ⇒ match b with 
                 [ sbase o' l' ⇒ (Operatoreqb o o') ∧ 
                                    (* Quella che segue deve essere 
                                    un po' sofisticata. *) 
                                    (ListAtomDeqSeteqb l l') 
                 | _           ⇒ false]
  | sind  o l ⇒ match b with 
                 [ sind o' l'  ⇒ (Operatoreqb o o') ∧ 
                                    (* Quella che segue deve essere 
                                     ancora più sofisticata della
                                     precedente. *) 
                                    (ListAtomDeqSeteqb l l')
                 | _           ⇒ false] ].
               
notation < "a == b" non associative with precedence 45 for @{Atomeqb $a $b }.

lemma Structureqb_true: ∀a,b. iff (Structureeqb a b = true) (a = b).
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .

(* Grazie al lemma precedente ho che gli Atomi formano un insieme
con equivalenza decidibile. *)
definition AtomDeqSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

let rec Structureneg (s:Structure) on s : Structure ≝ 
match s with 
[ unit      ⇒ unit
| sbase o l ⇒ match o with
               [ par ⇒ (sbase cop (map ?? Atomneg l))
               | seq ⇒ (sbase seq (map ?? Atomneg l))
               | cop ⇒ (sbase par (map ?? Atomneg l))]
| sind o l  ⇒ match o with
              [ par ⇒ match l with 
                      [ nil      ⇒ sind cop []
                      | cons h t ⇒ sind cop 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]
              | seq ⇒ match l with 
                      [ nil      ⇒ sind seq []
                      | cons h t ⇒ sind seq 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]
              | cop ⇒ match l with 
                      [ nil      ⇒ sind par []
                      | cons h t ⇒ sind par 
                                        ((Structureneg h):: 
                                          (map ?? Structureneg t))]  
             ]
].


(* Il principio di induzione potrebbe essere tipo il seguente. *)
theorem Structure_induction: 
∀P:Structure → Prop. 
    P unit → 
    (∀o:Operator. P (sbase o [])) → 
    (∀o:Operator.∀l:list AtomDeqSet. P (sbase o l)) →
    (∀o:Operator. P (sind o [])) → 
    (∀o:Operator.∀h:Structure.∀t:list Structure. 
        P h → P (sind o t) → P (sind o (h::t))) → 
    (∀s:Structure. P s) .
(* da fare *)


(* check Structureneg. *)

(* Da dimostrare a pezzi sfruttando Structure_induction alla fine. *)
lemma Structureneg_idem: ∀s:Structure. Structureneg (Structureneg s) = s.
#s cases s 
[ normalize @refl ] (* Primo goal *)
#L elim L 
[1,3,5,7,9,11: normalize @eq_f @refl
|2,4,6: #Hh #Ht 
 cases Hh #N #Hind normalize
  @eq_f @eq_f  (* ??????? *)
 ]
]  qed .


definition Structureeqb ≝ λa,b:Atom.
notation < "a ≡ b" non associative with precedence 45 for @{Atomeqb $a $b }.

let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].



(**********************************************************)
(* Abbozzo di una possibile strada alternativa
per definire le strutture. *)
definition Atomword ≝ list AtomDeqSet.
definition AtomBag1 ≝ [ 𝔸 \sub 1; 𝔹 \sub 2 ].

(* Unit: notation and interpretation *)
interpretation "Unit" 'Unit = (nil AtomDeqSet).
notation "𝟙" non associative with precedence 90 for @{ 'Unit }.
(* check 𝟙. *)

(* Par *)
inductive Par (A,B:Prop) : Prop ≝
    mkPar : A → B → Par A B.
(* Seq *)
inductive Seq (A,B:Prop) : Prop ≝
    mkSeq : A → B → Seq A B.
(* CoP *)
inductive CoP (A,B:Prop) : Prop ≝
    mkCoP : A → B → CoP A B.

(**********************************************************)
(* Altro abbozzo di definizione alternativa per la definizione
delle strutture. *)
definition name   ≝ λA:Type[0].λx,a:A.〈 x=a, true 〉.
interpretation "name" 'name x = (name ? x).
notation "x+" with precedence 100 for @{name $x}.  
definition coname ≝ λA:Type[0].λx,a:A.〈 x=a, false 〉.
interpretation "singleton" 'coname x = (coname ? x).
notation "x-" with precedence 100 for @{coname $x}.

(* check name.   *)
definition a_a ≝ name nat 1. definition a_b ≝ name nat 2.
definition a_c ≝ name nat 3. definition a_d ≝ name nat 4.
definition ca_a ≝ coname nat 1. definition ca_b ≝ coname nat 2.
definition ca_c ≝ coname nat 3. definition ca_d ≝ coname nat 4.

inductive operator : Type[0] ≝
  mkpar : operator
| mkcopar : operator
| mkseq : operator.  